T:Type, L:(T List), f:({0..||L||}T).
(i:{0..||L||}. f(i) = L[i])  (L = map(f;upto(||L||))) 

latex

Definitions	[], type List, , s = t, f(a), l[i], P  Q, i  j , {x:A| B(x)} , [car / cdr], x:AB(x), Type, {i..j}, n+m, ||as||, x:A. B(x), #$n, t  T, x.A(x), Void, x:A  B(x), a < b, , i  j < k, A  B, P & Q, A, False, P  Q, P  Q, T, True, n - m, s ~ t, , upto(n), Top, x:A.B(x), (i = j), i z j, i <z j, hd(l), S  T, f o g
Lemmas	top wf, map-map, upto wf, map append sq, upto decomp, squash wf, select cons tl, le wf, length wf1, int seg wf, non neg length, length cons, select wf, length wf2